This paper provides the first program logic for homogeneous generativerun-time meta-programming---using a variant of MiniML by Davies and Pfenning asits underlying meta-programming language. We show the applicability of ourapproach by reasoning about example meta-programs from the literature. We alsodemonstrate that our logics are relatively complete in the sense of Cook,enable the inductive derivation of characteristic formulae, and exactly capturethe observational properties induced by the operational semantics.
展开▼
